#include <iostream>
#include <stdlib.h>
#include <string>
#include <signal.h>

#include "node.h"
#include "generalizer.h"
#include "input.h"
#include "prover.h"
#include "server.h"
#include "system.h"
#include "try.h"

bool displayQueryResult (Rules &rules, Globals &globals, std::string query,
    bool elaborate = false) {
  bool ret;
  pNode node, generalized;
  Trail trail;
  Generalizer generalizer;
  System system (rules, globals, trail);

  // We must hold a pointer to original node, otherwise the variable name atoms
  //  might be cleaned from atom pool
  node = query;
  generalized = generalizer.generalize (*node);
  Prover *prover = Prover::create (*generalized, system);

  try {

    // Elaborate all answers if using slash
    if(elaborate) {
      int nSolutions = 0;
      while(prover->prove ()) {
        if(generalizer.nVariables ())
          std::cout << generalizer.dump () << std::endl;
        nSolutions++;
      }
      std::cout << nSolutions << (nSolutions == 1 ? " solution" : " solutions")
          << std::endl;
      ret = nSolutions != 0;
    } else {
      ret = prover->prove ();
      std::cout << (ret ? "Yes" : "No") << std::endl;
    }
  } catch(RaisedException ex) {
    std::cerr << "[ERROR] Caught exception: " << ex.node.node->dump ()
        << std::endl;
  }

  std::cout << std::endl;

  delete prover;
  return ret;
}

int main (int argc, char **argv) {

  // Ignore broken pipes, for network server implementation
  signal (SIGPIPE, SIG_IGN);

  // Gets singlog path to load rules
  char *path = getenv ("SINGLOGHOME");
  if(path)
    Input::singlogPath = path;
  else {
    // Gets executable directory as our loading path
    char *thisFile = argv[0], *slash = strrchr (thisFile, '/');
    if(slash)
      Input::singlogPath = std::string (thisFile, slash);
  }

  bool quit = false;

  {
    char *query = 0;
    pNode node;
    Rules rules;
    Globals globals;
    std::string input, line;
    SinglogServerThread serverThread (rules, globals);

    { // Import files by default and from parameters
      Trail trail;
      System loader (rules, globals, trail);

      // Try load the pre-compiled version first, normal rules otherwise
      loader.load ("%/auto.slb") || loader.load ("%/auto.sl");

      for(int arg = 1; arg < argc; arg++) {
        char first = argv[arg][0];
        if(first == '?' || first == '=')
          query = argv[arg] + 1;
        else if(strcmp (argv[arg], "-server") == 0) // singlog server
          serverThread.start ();
        else if(first == '-')
          rules.assertz (node = std::string (argv[arg] + 1));
        else if(!loader.load (argv[arg]))
          std::cout << "Failed to load: " << argv[arg] << std::endl;
      }
    }

    if(query)
      // Reversed; code 0 is normal
      return displayQueryResult (rules, globals, query) ? 0 : 1;

    // Initializes readline, with rule name completion function
    Input::setCommandCompletion (rules);

    while(!quit) {
      input.clear ();

      while(input.length () == 0 || *(input.end () - 1) != endOfRuleMarker) {
        quit = !Input::getLine (line, input.empty ());
        if(quit)
          goto endLoop;
        else {
          if(!input.empty () && line.empty ()) // Double-Enter ends a rule
            line = endOfRuleMarker;
          Input::concatLine (input, line);
        }
      }

      input = removeComments (input);
      if(input.length ()) // Eats ending terminator
        input = input.substr (0, input.length () - 1);

      if(!input.empty ())
        switch(input[0]) {
        case '?': // A yes or no query
          displayQueryResult (rules, globals, input.substr (1), false);
          break;

        case '/': // For lazy bugs who hate pressing Shifts
          displayQueryResult (rules, globals, input.substr (1), true);
          break;

        default: // Otherwise, a rule input
          node = input;
          // cout << node.display () << endl; // No echoes
          rules.assertz (node);
        }

      endLoop: ;
    }
  }

  return 0;
}
